Definitions	Unit, t  T, P  Q, P  Q, x:A. B(x), P  Q, P  Q, (x  l), x:A. B(x),
Lemmas	finite-type-iff-list, l member wf, member singleton, unit wf, it wf